;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "MResize.lisp")
(require "Mimage.lisp")
(require "MCommon.lisp")
;(require "timage.lisp")

(module TResize
  (include-book "list-utilities" :dir :teachpacks)
  (include-book "io-utilities" :dir :teachpacks)
  (include-book "avl-rational-keys" :dir :teachpacks)
  (include-book "doublecheck" :dir :teachpacks)
  (include-book "testing" :dir :teachpacks)
  
  (import ICommon)
  (import IImage)
  (import IResize)
  ;(import TImage)
  
  (defconst *header* (list 1 2 3 4 5 6))
  (defconst *tree1*   (avl-insert (avl-insert (avl-insert (empty-tree) -1 *header*) -2  2) -3 2))
  (defconst *newTree* (avl-insert (avl-insert (avl-insert (empty-tree) -1 *header*) -2 4) -3 4))
  (defconst *tree2* (insertPixel *tree1* 1 2 100 100 100))
  (defconst *tree3* (insertPixel *tree2* 2 2 105 105 105))
  (defconst *tree4* (insertPixel *tree3* 1 1 110 110 110))
  (defconst *tree5* (insertPixel *tree4* 2 1 115 115 115))
  (defconst *matchingRowPixels* (list (list (list 3 6 (list 133 213 223))
                                            (list 7 6 (list 136 231 249))
                                            (list 11 6 (list 239 139 123))
                                            (list 15 6 (list 211 122 133)))
                                      (list (list 3 4 (list 231 123 222))
                                            (list 7 4 (list 245 234 124))
                                            (list 11 4 (list 255 255 255))
                                            (list 15 4 (list 122 131 145)))
                                      (list (list 3 2 (list 100 100 100))
                                            (list 7 2 (list 105 105 105))
                                            (list 11 2 (list 110 110 110))
                                            (list 15 2 (list 115 115 115)))))
  (defconst *tree1Shrk* (avl-insert (avl-insert (avl-insert (empty-tree) -1 *header*) -2  4) -3 4))
  (defconst *tree2Shrk* (insertPixel (insertPixel (insertPixel (insertPixel *tree1Shrk* 4 4 103 103 103) 3 4 102 102 102) 2 4 101 101 101) 1 4 100 100 100))
  (defconst *tree3Shrk* (insertPixel (insertPixel (insertPixel (insertPixel *tree2Shrk* 4 3 105 105 105) 3 3 106 106 106) 2 3 107 107 107) 1 3 108 108 108))
  (defconst *tree4Shrk* (insertPixel (insertPixel (insertPixel (insertPixel *tree3Shrk* 4 2 109 109 109) 3 2 110 110 110) 2 2 111 111 111) 1 2 112 112 112))
  (defconst *tree5Shrk* (insertPixel (insertPixel (insertPixel (insertPixel *tree4Shrk* 4 1 113 113 113) 3 1 114 114 114) 2 1 115 115 115) 1 1 116 116 116))
  (defconst *newTreeShrk* (avl-insert (avl-insert (avl-insert (empty-tree) -1 *header*) -2 2) -3 2))
  
  
  
  
  
  ;  (check-expect  (calcBilinear 200 230 130 108 5 10 8 4 5 8) 200)
  ;  (check-expect  (tree? (calcAndInsertPix *tree1*
  ;                                          (list 200 234 199)
  ;                                          (list 230 177 182)
  ;                                          (list 130 255 239)
  ;                                          (list 108 245 230) 5 10 8 4 5 8)) t)
  ;  (check-expect (validCord 4 3 1 2) t)
  ;  (check-expect (calcNextY 3 t) 2)
  ;  (check-expect (car (calcNextX 2 1 4)) 3)
  ;  (check-expect (tree? (bilinearInterpolateSquare *tree1*
  ;                                                  (list 231 123 222)
  ;                                                  (list 245 234 124)
  ;                                                  (list 255 255 255)
  ;                                                  (list 122 131 145) 6 10 5 8 6 10)) t)
  ;  (check-expect (car (car (car (getListOfMatchingRowPix (list (list 1 3 '(231 123 222))
  ;                                                              (list 2 3 '(245 234 124))
  ;                                                              (list 3 3 '(255 255 255))
  ;                                                              (list 1 2 '(122 131 145))
  ;                                                              (list 3 2 '(200 234 199))) 3 '() '())))) 1)
  ;  (check-expect (tree? (cadr (insertOldElements *newTree* *tree5* '() 1 8 8 8 (list 2 0) (list 2 0)))) t)
  ;  (check-expect (tree? (interPolateBottomRightCorner *newTree* (list 7 7 (list 230 213 133)) 5 5)) t)
  ;  (check-expect (tree? (interPolateRightSection *newTree* (list (list 15 6 (list 133 213 223))
  ;                                                                (list 15 4 (list 136 231 249))
  ;                                                                (list 15 2 (list 239 139 123))) 2 2)) t)
  ;  (check-expect (tree? (interPolateBottomSection *newTree* (list (list 3 6 (list 133 213 223))
  ;                                                                 (list 7 6 (list 136 231 249))
  ;                                                                 (list 11 6 (list 239 139 123))
  ;                                                                 (list 15 6 (list 211 122 133))) 3 3 '() '())) t)
  ;  (check-expect (tree? (interPolateRowMainSection *newTree* (list (list 3 6 (list 133 213 223))
  ;                                                                  (list 7 6 (list 136 231 249))
  ;                                                                  (list 11 6 (list 239 139 123))
  ;                                                                  (list 15 6 (list 211 122 133))) 
  ;                                                  (list (list 3 4 (list 231 123 222))
  ;                                                        (list 7 4 (list 245 234 124))
  ;                                                        (list 11 4 (list 255 255 255))
  ;                                                        (list 15 4 (list 122 131 145))) 3 3 '() '())) t)
  ;  (check-expect (tree? (interPolateMainSection *newTree* *matchingRowPixels* 3 3))  t)
  ;  (check-expect (car (car (getFarRightColumn *matchingRowPixels* '()))) 15)
  ;  (check-expect (listp (car (createNewTree *tree5* *newTree* 16 8 8 (list 2 0) (list 2 0)))) t)
  ;  (check-expect (car (car (calcPercentIncrease 8 8 16 16))) 2)
  ;  (check-expect (tree? (car (resizeProportional *tree5* 2 2 4 4))) t)
  ;  (check-expect (car (getRGBAverage (list (list 2 5 3) (list 5 7 1) (list 5 2 9)) 3 0 0 0)) 4)
  ;  (check-expect (length (getPixelVals (list (list  1 2) (list 2 2) (list 1 1)) *tree5* '())) 3)
  ;  (check-expect (validCordShrink 2 2 2 3) nil)
  ;  (check-expect (calcNextYShrink 4 t) 3)
  ;  (check-expect (car (calcNextXShrink 2 1 4)) 3)
  ;  (check-expect (length (getCoordinates '() 5 14 8 16 5 16)) 12)
  ;  (check-expect (length (calcCoordinates 5 16 4 3 1 1 20 20)) 12)
  ;  (check-expect (tree? (insertCalculatedElements *newTreeShrk* *tree5Shrk* 1 2 2 2 2 2 0 0)) t)
  ;  (check-expect (car (getPixel (createNewTreeShrink *tree5Shrk* 2 2 2 2 0 0) 1 2)) 104)
  ;  (check-expect (cadr (getPixel (car (shrinkResize *tree5Shrk* 4 4 2 2)) 1 2)) 104)
  ;  (check-expect (tree? (car (checkShrinkOrExpand *tree5Shrk* 4 4 2 2))) t)
  ;  (check-expect (tree? (car (MainResize *tree5Shrk* (list 2 2)))) t)
  
  
  (defproperty calcBilinear-returns-integer 
    (Q11Val :where (integerp Q11Val) :value (random-between 0 255)
            Q21Val :where (integerp Q21Val) :value (random-between 0 255)
            Q12Val :where (integerp Q12Val) :value (random-between 0 255)
            Q22Val :where (integerp Q22Val) :value (random-between 0 255))
    (equal (integerp (calcBilinear Q11Val Q21Val Q12Val Q22Val 1 4 4 1 1 4)) t))
  
  
  (defrandom incrimenting-alist ()
    (let* ((elem1 (random-between 0 255))
           (elem2 (random-between 0 255))
           (elem3 (random-between 0 255)))
      (list elem1 elem2 elem3)))
  
  
  (defproperty calcAndInsertPix-returns-tree 
    (Q11 :where (listp Q11) :value (incrimenting-alist)
         Q21 :where (listp Q21) :value (incrimenting-alist)
         Q12 :where (listp Q12) :value (incrimenting-alist)
         Q22 :where (listp Q22) :value (incrimenting-alist))
    (equal (tree? (calcAndInsertPix *newTree* Q11 Q21 Q12 Q22 1 4 4 1 1 4)) t))
  
  
  (defproperty validCord-returns-boolean
    (nextX :where (integerp nextX) :value (random-between 0 4)
           nextY :where (integerp nextY) :value (random-between 0 4)
           beginWidth :where (booleanp beginWidth) :value (random-boolean)
           height :where (integerp height) :value (random-between 0 5))
    (equal (booleanp (validCord nextX nextY beginWidth height)) t))
  
  (defproperty calcNextY-returns-integer
    (y :where (integerp y) :value (random-integer)
       endOfX :where (booleanp endOfX) :value (random-boolean))
    (equal (integerp (calcNextY y endOfX)) t))
  
  (defproperty calcnextX-returns-integer
    (x :where (integerp x) :value (random-between 0 4))
    (equal (listp (calcNextX x 0 4)) t))
  
  
  (defproperty bilinearInterpolateSquare-returns-tree
    (Q11 :where (listp Q11) :value (incrimenting-alist)
         Q21 :where (listp Q21) :value (incrimenting-alist)
         Q12 :where (listp Q12) :value (incrimenting-alist)
         Q22 :where (listp Q22) :value (incrimenting-alist)
         x1  :where (integerp x1) :value (random-between 1 4)
         x2  :where (integerp x2) :value (random-between 6 10)
         y1  :where (integerp y1) :value (random-between 1 4)
         y2  :where (integerp y2) :value (random-between 6 10))
    (equal (tree? (bilinearInterpolateSquare *newTree* Q11 Q21 Q12 Q22 x1 x2 y1 y2 x1 y2)) t))
  
  (defrandom mixedList (rowNum)
    (let* ((elem1 (list (random-between 0 4) rowNum (list (random-between 0 255) (random-between 0 255) (random-between 0 255))))
           (elem2 (list (random-between 0 4) rowNum (list (random-between 0 255) (random-between 0 255) (random-between 0 255))))
           (elem3 (list (random-between 0 4) rowNum (list (random-between 0 255) (random-between 0 255) (random-between 0 255)))))
      (append (list elem1) (list elem2) (list elem3))))
  
  (defproperty getListOfMatchingRowPix-second-rowis-two 
    (row1 :where (listp row1) :value (mixedList 1)
          row2 :where (listp row2) :value (mixedList 2)
          row3 :where (listp row3) :value (mixedList 3)
          finalList :where (listp finalList) :value (append row1 row2 row3))
    (equal (cadr (car (cadr (getListOfMatchingRowPix finalList 1 '() '())))) 2))
  
  
  (defproperty  interPolateBottomRightCorner-returns-tree
    (randPixel :where (listp randPixel) :value (list (random-between 0 255) (random-between 0 255) (random-between 0 255)))
    (equal (tree? (interPolateBottomRightCorner *newTree* (list 2 2 randPixel) 2 2)) t))
  
  (defproperty interPolateRightSection-returns-tree
    (elem1 :where (listp elem1) :value (list 4 4 (list (random-between 0 255) (random-between 0 255) (random-between 0 255)))
           elem2 :where (listp elem1) :value (list 4 2 (list (random-between 0 255) (random-between 0 255) (random-between 0 255)))
           finalList :where (listp finalList) :value (append  (list elem1) (list elem2)))
    (equal (tree? (interPolateRightSection *newTree* finalList 1 1)) t))
  
  
  (defproperty interPolateBottomSection-returns-tree
    (elem1 :where (listp elem1) :value (list 2 4 (list (random-between 0 255) (random-between 0 255) (random-between 0 255)))
           elem2 :where (listp elem1) :value (list 4 4 (list (random-between 0 255) (random-between 0 255) (random-between 0 255)))
           finalList :where (listp finalList) :value (append  (list elem1) (list elem2)))
    (equal (tree? (interPolateBottomSection *newTree* finalList 2 2 '() '())) t))
  
  
  
  (defproperty interPolateRowMainSection-returns-tree
    (elem1 :where (listp elem1) :value (list 2 4 (list (random-between 0 255) (random-between 0 255) (random-between 0 255)))
           elem2 :where (listp elem1) :value (list 4 4 (list (random-between 0 255) (random-between 0 255) (random-between 0 255)))
           elem3 :where (listp elem1) :value (list 2 2 (list (random-between 0 255) (random-between 0 255) (random-between 0 255)))
           elem4 :where (listp elem1) :value (list 4 2 (list (random-between 0 255) (random-between 0 255) (random-between 0 255)))
           mainRow :where (listp mainRow) :value (append  (list elem1) (list elem2))
           secondRow :where (listp secondRow) :value (append  (list elem3) (list elem4)))
    (equal (tree? (interPolateRowMainSection *newTree* mainRow secondRow 2 2 '() '())) t))
  
  
  (defproperty interPolateMainSection-returns-tree
    (elem1 :where (listp elem1) :value (list 2 4 (list (random-between 0 255) (random-between 0 255) (random-between 0 255)))
           elem2 :where (listp elem1) :value (list 4 4 (list (random-between 0 255) (random-between 0 255) (random-between 0 255)))
           elem3 :where (listp elem1) :value (list 2 2 (list (random-between 0 255) (random-between 0 255) (random-between 0 255)))
           elem4 :where (listp elem1) :value (list 4 2 (list (random-between 0 255) (random-between 0 255) (random-between 0 255)))
           mainRow :where (listp mainRow) :value (append  (list elem1) (list elem2))
           secondRow :where (listp secondRow) :value (append  (list elem3) (list elem4))
           finalList :where (listp finalList) :value (append  (list mainRow) (list secondRow)))
    (equal (tree? (interPolateMainSection *newTree* finallist 2 2)) t))
  
  (defproperty getFarRightColumn-has-size-equal-to-number-of-rows
    (row1 :where (listp row1) :value (mixedList 1)
          row2 :where (listp row2) :value (mixedList 2)
          row3 :where (listp row3) :value (mixedList 3)
          row4 :where (listp row4) :value (mixedList 4)
          finalList :where (listp finalList) :value (append row1 row2 row3 row4))
    (equal (len (getFarRightColumn finalList '())) (len finalList)))
  
  (defrandom makeTree (treeWidth treeHeight)
    (let* ((returnTree (avl-insert (avl-insert (avl-insert (empty-tree) -1 *header*) -2 treeWidth) -3 treeHeight)))
      returnTree))
  
    (defproperty  insertOldElements-inserts-in-right-location
      (inputTree :value *tree5*
                  xLoc :value (random-between 1 2)
                  yLoc :value (random-between 1 2)
                  newXLoc :value (* xLoc 2)
                  newYLoc :value (* yLoc 2))
      (equal (cdr (avl-retrieve (cdr (avl-retrieve (cadr (insertOldElements *newTree* *tree5* '() 1 2 2 2 (list 2 0) (list 2 0))) newYLoc)) newXLoc))
              (cdr (avl-retrieve (cdr (avl-retrieve inputTree yLoc)) xLoc))))
  
  
 ; (defproperty createNewTree-returns-a-tree
 ;   (
     
     ;createNewTree (tree newTreeWidth newTreeHeight oldTreeWidth oldTreeHeight percentIncreaseW percentIncreaseH)
  
  (defproperty calcPercentIncrease-returns-div-current-width-and-newWidth
    (currentTreeWidth :value (random-between 4 32)
                      currentTreeHeight :value (random-between 4 32)
                      newWidth   :value (random-between 32 64)
                      newHeight  :value (random-between 32 64))
    (equal (car (car (calcPercentIncrease currentTreeWidth currentTreeHeight newWidth newHeight))) (/ newWidth currentTreeWidth)))
  
  (defrandom getRandomListOfPixels (sizeOfList returnList)
    (let* ((num1 (random-between 1 255))
           (num2 (random-between 1 255))
           (num3 (random-between 1 255))
           (pixelList (list num1 num2 num3)))
      (if (equal sizeOfList 1)
          (append returnList (list pixelList))
          (getRandomListOfPixels (- sizeOfList 1) (append returnList (list pixelList))))))
  
  
  (defproperty getRGBAverage-returns-integer-listp
    (repBoxSize :value (random-between 2 10)
                oldTreePixelVals :value (getRandomListOfPixels repBoxSize '()))
    (equal (integer-listp (getRGBAverage oldTreePixelVals repBoxSize 0 0 0)) t))
  
  (defproperty getPixelVals-returns-a-list-of-lists-of-length-equal-to-inputcords-length
    (coordinates :value (getCoordinates '() 1 1 2 2 1 2)
          randElement :value (random-Between 1 4))
    (equal (LEN (getPixelVals coordinates *tree5* '())) (LEN coordinates)))
  
  (defproperty validCordShirink-returns-true-when-nextY-is-Less-than-height
    (height :value (random-between 4 8)
            nextY :value (random-between 1 (- height 1)))
    (equal (validCordShrink 1 nextY 1 height) nil))
  
    (defproperty  calcNextYShrink-returns-integer
    (y :where (integerp y) :value (random-integer)
       endOfX :where (booleanp endOfX) :value (random-boolean))
    (equal (integerp (calcNextYShrink y endOfX)) t))
  
    (defproperty calcNextXShrink-returns-integer
    (x :where (integerp x) :value (random-between 0 4))
    (equal (listp (calcNextXShrink x 0 4)) t))
          
    
    ;validCordShrink (nextX nextY beginWidth height)
    
    )
  (link RTResize
        (MCommon MImage MResize TResize))
  
  
  (invoke RTResize)